Section: New Results

Improvement of theoretical foundations

Algebraic rewriting

Participant : Yves Guiraud.

With P. Malbos (Institut Camille Jordan, Univ. Lyon 1), in [13] , we have used rewriting to give a theoretical setting and concrete formal methods to formalise and give constructive proofs of coherence theorems. The first one is Mac Lane's classical result on monoidal categories: the new proof we give is a direct application of [7] . Then, cases like symmetric monoidal categories are a first step towards a “rewriting modulo” version of the same work. Finally, we give a new understanding and a constructive proof of the result for cases like braided monoidal categories.

With P. Malbos, in [14] , we have generalised the work of [7] to any dimension. We have introduced a notion of polygraphic resolution that generalises both usual algebraic resolutions, in combinatorial algebra, but also, more surprisingly, normalisation strategies, as used in rewriting theory and, in particular, in rule-based programming languages. Thus, a functional program can be mathematically defined as a complete cellular model of the functions it computes. This gives a strong mathematical background to the notion of program, together with a constructive way to build resolutions from convergent polygraphs. This work has been presented during an invited conference at the International Congress on Operads and Universal Algebra, held in Tianjin, China, in July 2010. Those results will be further explored to give a mathematical description of the strategies used in Tom, in order to develop methods from algebraic topology to study their computational properties, like termination and complexity.

With S. Gaussent (Institut Élie Cartan, Univ. Nancy 1) and P. Malbos, in [26] , we have applied higher-dimensional rewriting methods to actions of monoids on categories. The objective was to compute, starting from a presentation of a monoid by generators and relations, a “homotopy basis” that generates all the relations between the relations: this is exactly the piece of data one needs to use a presentation to give a practical definition of action of the monoid on categories. We show that methods from rewriting theory (Squier's theorem, Knuth-Bendix completion procedure), adapted to Burroni's polygraphs, can be used to compute that homotopy basis. In particular, we get a new, algebraic and constructive proof of a result by Deligne on actions of braid groups.

Certification of induction proofs

Participant : Sorin Stratulat.

We have defined a methodology for validating implicit induction proofs. In collaboration with Vincent Demange, we gave evidence of the possibility to perform implicit induction-based proofs inside certified reasoning environments, as that provided by the Coq proof assistant. This is the first step of a long term project focused on 1) mechanically certifying implicit induction proofs generated by automated provers like Spike, and 2) narrowing the gap between automated and interactive proof techniques by devising powerful proof strategies inside proof assistants that aim to perform automatically multiple induction steps and to deal with mutual induction more conveniently. Contrary to the current approaches of reconstructing implicit induction proofs into scripts based on explicit induction tactics that integrate the usual proof assistants, our checking methodology is simpler and fits better for automation. The underlying implicit induction principles are separated and validated independently from the proof scripts that consist in a bunch of one-to-one translations of implicit induction proof steps. The translated steps can be checked independently, too, so the validation process fits well for parallelisation and for the management of large proof scripts. Moreover, our approach is more general; any kind of implicit induction proof can be considered because the limitations imposed by the proof reconstruction techniques no longer exist. This result has been firstly presented at the Poster session of 2010 Grande Region Security and Reliability Day, Saarbrucken.

Based on the previous result, an implementation that integrates automatic translators for generating fully checkable Coq scripts from Spike proofs is reported in  [55] . The induction ordering underlying the Spike induction principle was defined using COCCINELLE  [34] , a Coq library well suited for modelling mathematical notions needed for rewriting, such as term algebras and RPO. COCCINELLE formalises RPO in a generic way using a precedence and a status (multiset/lexicographic) for each function symbol. Spike automatically generates a term algebra starting from Coq function symbols which preserve the precedence of the original Spike symbols. Many useful properties about the RPO orderings have been already provided by COCCINELLE. On the other hand, the induction ordering was modelled as a multiset extension of RPO and only few properties about it were provided by COCCINELLE. We have proved useful lemmas about it and added them to COCCINELLE, for example, the multiset extensions of RPO is stable under substitutions. Finally, every single inference step derived with a restricted version of Spike can be automatically translated into equivalent Coq script. The restricted inference system was powerful enough to prove properties about specifications involving mutually defined functions and to validate a sorting algorithm. The scripts resulted from the translation of these proofs were successfully validated by Coq.

Another improvement of the COCCINELLE library was the redefinition of the RPO ordering in order to consider precedencies that take into account equivalent function symbols. The new release of CoLoR (http://color.inria.fr ) that compiles with the new version 8.3 of Coq includes the updated version of COCCINELLE. This improvement allowed Rainbow, a program developped within the CoLoR project that uses COCCINELLE's formalisation for RPO, to certify more than 30 additional proofs from the set of CPF files generated during the 2009 annual termination competition (http://termination-portal.org/wiki/Termination_Competition ).

In [21] , we reported new improvements in order to certify implicit induction proofs concerning industrial-size applications, in particular the validation proof of a conformance algorithm for the ABR protocol  [51] . An interactive proof using PVS  [54] was firstly presented in  [52] , then it has been shown in  [53] that more than a third of the user interactions can be avoided using implicit induction techniques, Spike succeeding to prove 60% of the user-provided lemmas automatically. Now, a simpler but more restrictive version of the Spike inference system has been shown powerful enough to prove 2/3 out of these lemmas. Moreover, any generated proof has been automatically translated into a Coq script, then automatically certified by Coq. We stressed the importance of the automatic feature since the proof scripts are in many cases big and hard to manipulate by the users. The bottom-line is that these improvements allowed us to certify big proof scripts in a reasonable time, 20 times faster than in  [55] .